Table of Contents

Concurrency Tool Comparison

Summary Results Table

replicated (5,2)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (97) 0.97 203.71s 716039.24 (0.00) 383.79 (360.53)
replicated (8,2)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (97) 0.97 4.77s 1800.77 (0.00) 1799.77 (1799.77)
JPF Stateless Random Walk 10159 (9632) 0.95 5.39s 134.49 (NA) 0.00 (NA)

Java Pathfinder

Stateless Random Walk

Parameters Path Error Density
8,2 0.948

one hour. A total of 100 computation hours dedicated in discovering the 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
(5,2) 100 (97) 97.00% 203.71s 716039.24 (0.00) 383.79 (360.53) 203712.19 3288.24 383.79 360.53 167602.51 548436.73 0.22 715677.71 167240.76 0.00 347472.49 6990528.00 109416.73 726.43 735.43
(8,2) 100 (97) 97.00% 4.77s 1800.77 (0.00) 1799.77 (1799.77) 4772.70 4772.70 1799.77 1799.77 1800.77 0.00 0.00 0.00 0.00 0.00 58443.22 6990528.00 0.00 764.00 805.82

CHESS

Parameters Time Transitions paths Max Depth
5, 2, 0, 10, 05 620 103 1 103
8, 2, 0, 10, 001 620 157 1 157