This shows you the differences between two versions of the page.
— |
vv-lab:accountdeadlock [2015/02/18 15:51] (current) egm created |
||
---|---|---|---|
Line 1: | Line 1: | ||
+ | [[Concurrency Tool Comparison]] | ||
+ | == Model Description == | ||
+ | |||
+ | The model exhibits a deadlock caused from a cyclic lock acquisition by a set of threads. | ||
+ | |||
+ | Classes: 3 | ||
+ | |||
+ | SLOC: 66 | ||
+ | |||
+ | Parameters: (numOfThreads) | ||
+ | |||
+ | == Summary Results Table == | ||
+ | |||
+ | {| align=center | border=1 | ||
+ | |- bgcolor="white" | | ||
+ | | colspan=5 align="center" | accountDeadlock (4) | ||
+ | |- bgcolor="lightblue" | ||
+ | ! Tool | ||
+ | ! Trials (successful) | ||
+ | ! Time | ||
+ | ! Transition (paths) | ||
+ | ! Max Depth (error depth) | ||
+ | |- | ||
+ | | CHESS | ||
+ | | 1 (1) 1.00 | ||
+ | | align="right"| 337.76s | ||
+ | | 13341480.00 (111179.00) | ||
+ | | 120.00 (NA) | ||
+ | |- | ||
+ | | ConTest | ||
+ | | 1000 (0) 0.00 | ||
+ | | align="right"| NA | ||
+ | | NA (NA) | ||
+ | | NA (NA) | ||
+ | |- bgcolor="white" | | ||
+ | | colspan=5 align="center" | accountDeadlock (5) | ||
+ | |- bgcolor="lightblue" | ||
+ | ! Tool | ||
+ | ! Trials (successful) | ||
+ | ! Time | ||
+ | ! Transition (paths) | ||
+ | ! Max Depth (error depth) | ||
+ | |- | ||
+ | | JPF "Randomized DFS" | ||
+ | | 5063 (1684) 0.33 | ||
+ | | align="right"| 479.82s | ||
+ | | 7386006.08 (0.00) | ||
+ | | 199.97 (114.10) | ||
+ | |- | ||
+ | | JPF Stateless Random Walk | ||
+ | | 10127 (780) 0.08 | ||
+ | | align="right"| NA | ||
+ | | NA (NA) | ||
+ | | NA (NA) | ||
+ | |- | ||
+ | | CHESS | ||
+ | | 1 (1) 1.00 | ||
+ | | align="right"| 473.11s | ||
+ | | 20602893.00 (136443.00) | ||
+ | | 151.00 (NA) | ||
+ | |- | ||
+ | | ConTest | ||
+ | | 1000 (0) 0.00 | ||
+ | | align="right"| 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. | ||
+ | |||
+ | ==Chess== | ||
+ | |||
+ | * ChessBound=2 | ||
+ | * ChessMonitorVolatiles=true | ||
+ | |||
+ | {| align=center | border=1 | -bgcolor=grey | ||
+ | ! Account Params !! Tests !! Found Error !! Time Taken !! Steps (Depth) | ||
+ | |- | ||
+ | | 4 || 272,034 || Yes (Deadlock) || 1554.581 secs || 176 | ||
+ | |- | ||
+ | | 5 || 292,460 || Yes (Deadlock) || 1872.823 secs || 221 | ||
+ | |} | ||
+ | |||
+ | * ChessMonitorVolatiles=false | ||
+ | |||
+ | {| align=center | border=1 | -bgcolor=grey | ||
+ | ! Account Params !! Tests !! Found Error !! Time Taken !! Steps (Depth) | ||
+ | |- | ||
+ | | 4 || 111,179 || Yes (Deadlock) || 337.757 secs || 120 | ||
+ | |- | ||
+ | | 5 || 136,443 || Yes (Deadlock) || 473.11 secs || 151 | ||
+ | |- | ||
+ | |} | ||
+ | |||
+ | ==Java PathFinder== | ||
+ | ===Stateless Random Walk=== | ||
+ | |||
+ | Source is pathErr | ||
+ | |||
+ | * 10,000 Trials of Random Walk | ||
+ | * The ratio of the error discovery trials over the total number of trials is the | ||
+ | |||
+ | {| 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 | ||
+ | |- | ||
+ | |() | ||
+ | | 10127 (780) 7.70% | ||
+ | | align="right"| 0.00s | ||
+ | | 0.00 (0.00) | ||
+ | | 0.00 (0.00) | ||
+ | | align="right" | 0.00 | ||
+ | | align="right" | 0.00 | ||
+ | | align="right" | 0.00 | ||
+ | | align="right" | 0.00 | ||
+ | | align="right" | 0.00 | ||
+ | | align="right" | 0.00 | ||
+ | | align="right" | 0.00 | ||
+ | | align="right" | 0.00 | ||
+ | | align="right" | 0.00 | ||
+ | | align="right" | 0.00 | ||
+ | | align="right" | 0.00 | ||
+ | | align="right" | 0.00 | ||
+ | | align="right" | 0.00 | ||
+ | | align="right" | 0.00 | ||
+ | | align="right" | 0.00 | ||
+ | |} | ||
+ | |||
+ | ===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). | ||
+ | |||
+ | Source is error_analysis | ||
+ | |||
+ | {| 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 head objects | ||
+ | |- | ||
+ | |() | ||
+ | | 5063 (1684) 33.26% | ||
+ | | align="right"| 479.82s | ||
+ | | 7386006.08 (0.00) | ||
+ | | 199.97 (114.10) | ||
+ | | align="right" | 479819.03 | ||
+ | | align="right" | 5020.64 | ||
+ | | align="right" | 199.97 | ||
+ | | align="right" | 114.10 | ||
+ | | align="right" | 1665631.08 | ||
+ | | align="right" | 5720375.00 | ||
+ | | align="right" | 10.19 | ||
+ | | align="right" | 7386005.08 | ||
+ | | align="right" | 1665218.32 | ||
+ | | align="right" | 1665218.32 | ||
+ | | align="right" | 390486.19 | ||
+ | | align="right" | 932096.00 | ||
+ | | align="right" | 183307.65 | ||
+ | | align="right" | 176.00 | ||
+ | | align="right" | 180.98 | ||
+ | |} | ||
+ | |||
+ | ==ConTest== | ||
+ | |||
+ | * 1000 independent trials | ||
+ | |||
+ | * The ratio of the error discovery trials over the total number of trials is the | ||
+ | path error density. | ||
+ | |||
+ | {| align=center | border=1 | -bgcolor=grey | ||
+ | ! Account Params !! Path Error Density | ||
+ | |- | ||
+ | | 4 || 0.000 | ||
+ | |- | ||
+ | | 5 || 0.000 | ||
+ | |} |