vv-lab:accountdeadlock [CS Wiki]

Differences

This shows you the differences between two versions of the page.

@@ 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
+|}

vv-lab/accountdeadlock.txt · Last modified: 2015/02/18 22:51 by egm

Back to top