Concurrency Tool Comparison

Model Description

A readers writers example that contains a race condition.

Classes: 6

SLOC: 103

Parameters (checkForDeadlock)

Summary Results Table

rwN ()
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 118 (94) 0.80 1.27s 575.14 (0.00) 574.14 (574.14)
JPF Stateless Random Walk 10181 (7820) 0.77 NA NA (NA) NA (NA)

Java PathFinder

Stateless Random Walk

  • 10,000 Trials of Random Walk
  • The ratio of the error discovery trials over the total number of trials is the

path error density.

No Exception Check

Parameters Path Error Density
default 0.076
  • 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).

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
(N) 118 (94) 79.66% 1.27s 575.14 (0.00) 574.14 (574.14) 1269.11 1269.11 574.14 574.14 575.14 0.00 0.00 0.00 0.00 0.00 17960.17 6990528.00 0.00 156.69 173.64

CHESS

Parameters Time Transitions paths Max Depth
2, 2, 100 391329 67920000 24000 2830
vv-lab/readerswriters.txt · Last modified: 2015/02/18 22:58 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