Concurrency Tool Comparison

Model Description

A race condition in producer and consumer model.

Classes: 8

SLOC: 87

Parameters: (#prod, #cons, #items)

Summary Results Table

producerconsumer (1,10,4)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 115 (84) 0.73 86.11s 963174.08 (0.00) 121.87 (116.52)
JPF Stateless Random Walk 10125 (5434) 0.54 1.22s 116.26 (NA) 0.00 (NA)
producerconsumer (1,12,4)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 135 (93) 0.69 146.54s 1677307.59 (0.00) 133.19 (128.74)
JPF Stateless Random Walk 10125 (5405) 0.53 1.26s 126.19 (NA) 0.00 (NA)
producerconsumer (1,16,4)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 4999 (2736) 0.55 25.65s 283379.04 (0.00) 146.74 (145.98)
JPF Stateless Random Walk 10113 (5380) 0.53 1.18s 146.01 (NA) 0.00 (NA)
producerconsumer (1,8,4)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 115 (111) 0.97 94.91s 1300588.95 (0.00) 113.86 (107.14)
JPF Stateless Random Walk 10122 (5389) 0.53 1.10s 105.43 (NA) 0.00 (NA)
producerconsumer (2,2,4)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 0.83s 120.42 (0.00) 99.09 (98.25)
JPF Stateless Random Walk 10124 (7760) 0.77 1.11s 98.42 (NA) 0.00 (NA)
producerconsumer (2,4,4)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 0.87s 120.46 (0.00) 110.75 (110.65)
JPF Stateless Random Walk 10126 (9680) 0.96 1.13s 111.14 (NA) 0.00 (NA)
producerconsumer (2,8,4)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 0.99s 593.74 (0.00) 135.70 (135.49)
JPF Stateless Random Walk 10126 (9799) 0.97 1.11s 134.56 (NA) 0.00 (NA)
producerconsumer (7,10,4)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 1.22s 370.09 (0.00) 369.09 (369.09)

Java Pathfinder

Stateless Random Walk

Parameters Path Error Density
1,8,4 0.532
1,10,4 0.537
1,12,4 0.534
1,16,4 0.531
2,2,4 0.767
2,2,4 0.956
2,8,4 0.967
  • 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
(1,12,4) 135 (93) 68.89% 146.54s 1677307.59 (0.00) 133.19 (128.74) 146535.80 1531.52 133.19 128.74 235782.88 1441524.71 1.20 1677177.85 235652.94 0.00 306280.60 6990528.00 141235.20 237.00 237.00
(2,8,4) 100 (100) 100.00% 0.99s 593.74 (0.00) 135.70 (135.49) 985.94 985.94 135.70 135.49 260.76 332.98 1.02 457.25 124.25 0.00 17381.76 6990528.00 0.00 225.07 225.07
(7,10,4) 100 (100) 100.00% 1.22s 370.09 (0.00) 369.09 (369.09) 1217.91 1217.91 369.09 369.09 370.09 0.00 1.00 0.00 0.00 0.00 17490.56 6990528.00 0.00 253.02 261.46
(2,2,4) 100 (100) 100.00% 0.83s 120.42 (0.00) 99.09 (98.25) 831.93 831.93 99.09 98.25 111.74 8.68 1.20 21.17 12.28 0.00 16512.00 6990528.00 0.00 200.93 200.93
(2,4,4) 100 (100) 100.00% 0.87s 120.46 (0.00) 110.75 (110.65) 865.74 865.74 110.75 110.65 115.66 4.80 1.03 8.81 3.98 0.00 16368.00 6990528.00 0.00 209.02 209.02
(1,8,4) 115 (111) 96.52% 94.91s 1300588.95 (0.00) 113.86 (107.14) 94906.75 3281.18 113.86 107.14 200326.51 1100262.43 1.49 1300480.80 200217.88 0.00 323747.17 6990528.00 108138.57 221.00 221.00
(1,16,4) 4999 (2736) 54.73% 25.65s 283379.04 (0.00) 146.74 (145.98) 25645.56 1081.17 146.74 145.98 38927.38 244451.65 1.03 283232.06 38780.38 0.00 24845.89 932096.00 4041.29 253.00 253.00
(1,10,4) 115 (84) 73.04% 86.11s 963174.08 (0.00) 121.87 (116.52) 86108.83 2191.33 121.87 116.52 138683.65 824490.43 1.30 963056.56 138565.83 0.00 209030.10 6990528.00 78466.30 229.00 229.00
vv-lab/producerconsumer.txt · Last modified: 2015/02/18 22:57 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