Differences

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

Link to this comparison view

vv-lab:accountdeadlock [2015/02/18 22: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
 +|}
vv-lab/accountdeadlock.txt ยท Last modified: 2015/02/18 22:51 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0