Back

Model Description

The model is designed to allocate and free blocks. The bug is manifested due a synchronization gap between two individually locked methods. Context-switching between these methods raises an Exception.

Classes: 3

SLOC: 85

Parameters: (blockSize, vectorSize, #runs)

Summary Results Table

allocate (2,100,1,2)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 7.67s 78569.50 (0.00) 78.29 (57.01)
allocate (2,100,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 7.67s 78569.50 (0.00) 78.29 (57.01)
CHESS 1 (1) 1.00 1.00s 216.00 (3.00) 72.00 (NA)
allocate (2,20,1,2)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 3.08s 13109.32 (0.00) 75.57 (56.05)
allocate (2,20,4,2)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 2.93s 15899.23 (0.00) 264.60 (248.12)
allocate (8,20,1,2)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (99) 0.99 34.69s 573020.90 (0.00) 194.87 (154.32)

Chess

  • ChessBound=2
  • ChessMonitorVolatiles=false
AllocationVector Params Tests Found Error Time Taken Steps (Depth)
2,100,1 3 Yes 0.4-1.0 secs 72

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.

Parameters Path Error Density
2,20,1 0.085
2,20,4 0.294
2,100,1 0.018
8,20,2 0.442
  • 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
(2,20,4,2) 100 (100) 100.00% 2.93s 15899.23 (0.00) 264.60 (248.12) 2932.76 2631.07 264.60 248.12 5645.77 10253.46 0.77 15650.11 5395.88 0.00 46645.76 6990528.00 1592.21 225.68 225.68
(8,20,1,2) 100 (99) 99.00% 34.69s 573020.90 (0.00) 194.87 (154.32) 34692.74 3028.96 194.87 154.32 198205.85 374815.05 0.49 572865.58 198050.03 0.00 213983.03 6990528.00 53879.25 194.00 194.00
(2,20,1,2) 100 (100) 100.00% 3.08s 13109.32 (0.00) 75.57 (56.05) 3082.10 2982.10 75.57 56.05 4832.29 8277.03 0.90 13052.27 4774.34 0.00 37712.00 6990528.00 309.38 194.00 194.00
(2,100,1,2) 100 (100) 100.00% 7.67s 78569.50 (0.00) 78.29 (57.01) 7667.78 4665.67 78.29 57.01 28406.49 50163.01 0.98 78511.49 28347.50 0.00 122312.32 6990528.00 24170.40 194.00 194.00
vv-lab/allocationvector.txt · Last modified: 2015/02/18 22:54 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