Table of Contents

Concurrency Tool Comparison

Model Description

A simple scheduler that contains an assertion violation.

Classes: 24

SLOC: 838

Parameters: (abs?)

Summary Results Table

deosA ()
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 2.87s 1184.21 (0.00) 39.98 (27.78)
JPF Stateless Random Walk 10129 (1925) 0.19 1.95s 9.03 (NA) 0.00 (NA)

Java Pathfinder

Stateless Random Walk

Parameters Path Error Density
a 0.190

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
(a) 100 (100) 100.00% 2.87s 1184.21 (0.00) 39.98 (27.78) 2874.56 2874.56 39.98 27.78 747.11 437.10 0.55 1155.43 718.78 0.00 38716.16 6990528.00 0.00 295.17 295.25