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

accountDeadlock (4)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
CHESS 1 (1) 1.00 337.76s 13341480.00 (111179.00) 120.00 (NA)
ConTest 1000 (0) 0.00 NA NA (NA) NA (NA)
accountDeadlock (5)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 5063 (1684) 0.33 479.82s 7386006.08 (0.00) 199.97 (114.10)
JPF Stateless Random Walk 10127 (780) 0.08 NA NA (NA) NA (NA)
CHESS 1 (1) 1.00 473.11s 20602893.00 (136443.00) 151.00 (NA)
ConTest 1000 (0) 0.00 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
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
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
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% 0.00s 0.00 (0.00) 0.00 (0.00) 0.00 0.00 0.00 0.00 0.00 0.00 0.00 0.00 0.00 0.00 0.00 0.00 0.00 0.00 0.00
  • 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

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% 479.82s 7386006.08 (0.00) 199.97 (114.10) 479819.03 5020.64 199.97 114.10 1665631.08 5720375.00 10.19 7386005.08 1665218.32 1665218.32 390486.19 932096.00 183307.65 176.00 180.98

ConTest

  • 1000 independent trials
  • The ratio of the error discovery trials over the total number of trials is the

path error density.

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