This shows you the differences between two versions of the page.
— |
vv-lab:linkedlist [2015/02/18 15:56] (current) egm created |
||
---|---|---|---|
Line 1: | Line 1: | ||
+ | [[Concurrency Tool Comparison]] | ||
+ | == 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 == | ||
+ | |||
+ | {| align=center | border=1 | ||
+ | |- bgcolor="white" | | ||
+ | | colspan=5 align="center" | linkedlist (4,100) | ||
+ | |- bgcolor="lightblue" | ||
+ | ! Tool | ||
+ | ! Trials (successful) | ||
+ | ! Time | ||
+ | ! Transition (paths) | ||
+ | ! Max Depth (error depth) | ||
+ | |- | ||
+ | | JPF "Randomized DFS" | ||
+ | | 100 (100) 1.00 | ||
+ | | align="right"| 10.51s | ||
+ | | 10031.57 (0.00) | ||
+ | | 9993.02 (9990.94) | ||
+ | |- | ||
+ | | JPF Stateless Random Walk | ||
+ | | 10157 (9988) 0.98 | ||
+ | | align="right"| 9.29s | ||
+ | | 9937.49 (NA) | ||
+ | | 0.00 (NA) | ||
+ | |} | ||
+ | |||
+ | ==CHESS== | ||
+ | {| align=center | border=1 | | ||
+ | |- bgcolor="lightblue" | ||
+ | ! Parameters !! Time !! Transitions !! paths !! Max Depth | ||
+ | |- | ||
+ | | 2, 20 || 3447 || 347600 || 400 || 869 | ||
+ | |- | ||
+ | | 4, 100 || 1450576 || 281497000 || 23000 || 12239 | ||
+ | |} | ||
+ | |||
+ | ==Java Pathfinder== | ||
+ | ===Stateless Random Walk=== | ||
+ | |||
+ | {| align=center | border=1 | -bgcolor=grey | ||
+ | ! 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). | ||
+ | {| 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 | ||
+ | |||
+ | |- | ||
+ | |(4,100) | ||
+ | | 100 (100) 100.00% | ||
+ | | align="right"| 10.51s | ||
+ | | 10031.57 (0.00) | ||
+ | | 9993.02 (9990.94) | ||
+ | | align="right" | 10510.54 | ||
+ | | align="right" | 5309.57 | ||
+ | | align="right" | 9993.02 | ||
+ | | align="right" | 9990.94 | ||
+ | | align="right" | 10014.32 | ||
+ | | align="right" | 17.25 | ||
+ | | align="right" | 1.02 | ||
+ | | align="right" | 39.63 | ||
+ | | align="right" | 22.36 | ||
+ | | align="right" | 0.00 | ||
+ | | align="right" | 78468.48 | ||
+ | | align="right" | 6990528.00 | ||
+ | | align="right" | 12790.96 | ||
+ | | align="right" | 388.80 | ||
+ | | align="right" | 388.80 | ||
+ | |} |