Differences

This shows you the differences between two versions of the page.

Link to this comparison view

vv-lab:allocationvector [2015/02/18 22:54] (current)
egm created
Line 1: Line 1:
 +[[Concurrency Tool Comparison | 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 ==
 +
 +{| align=center | border=1
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | allocate (2,100,1,2)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 100 (100) 1.00
 +| align="​right"​| 7.67s
 +| 78569.50 (0.00)
 +| 78.29 (57.01)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | allocate (2,100,1)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 100 (100) 1.00
 +| align="​right"​| 7.67s
 +| 78569.50 (0.00)
 +| 78.29 (57.01)
 +|-
 +| CHESS
 +| 1 (1) 1.00
 +| align="​right"​| 1.00s
 +| 216.00 (3.00)
 +| 72.00 (NA)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | allocate (2,20,1,2)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 100 (100) 1.00
 +| align="​right"​| 3.08s
 +| 13109.32 (0.00)
 +| 75.57 (56.05)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | allocate (2,20,4,2)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 100 (100) 1.00
 +| align="​right"​| 2.93s
 +| 15899.23 (0.00)
 +| 264.60 (248.12)
 +|- bgcolor="​white"​ |
 +| colspan=5 align="​center"​ | allocate (8,20,1,2)
 +|- bgcolor="​lightblue"​
 +! Tool
 +! Trials (successful)
 +! Time
 +! Transition (paths)
 +! Max Depth (error depth)
 +|-
 +| JPF "​Randomized DFS"
 +| 100 (99) 0.99
 +| align="​right"​| 34.69s
 +| 573020.90 (0.00)
 +| 194.87 (154.32)
 +|}
 +==Chess==
 +
 +* ChessBound=2
 +* ChessMonitorVolatiles=false
 +
 +{| align=center | border=1 | -bgcolor=grey
 +! 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. ​
 +
 +{| align=center | border=1 | -bgcolor=grey
 +! Parameters !! Path Error Density
 +|- 
 +| 2,20,1 || 0.085
 +|-
 +| 2,20,4 || 0.294
 +|-
 +| 2,100,1 || 0.018
 +|-
 +| 8,20,2 || 0.442
 +|}
 +
 +===Stateful Randomized Depth-first search===
 +
 +* 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). ​
 +{| align="​center"​ | border=1
 +|- bgcolor="​lightblue"​
 +! 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%
 +| align="​right"​| 2.93s
 +| 15899.23 (0.00)
 +| 264.60 (248.12)
 +| align="​right"​ | 2932.76
 +| align="​right"​ | 2631.07
 +| align="​right"​ | 264.60
 +| align="​right"​ | 248.12
 +| align="​right"​ | 5645.77
 +| align="​right"​ | 10253.46
 +| align="​right"​ | 0.77
 +| align="​right"​ | 15650.11
 +| align="​right"​ | 5395.88
 +| align="​right"​ | 0.00
 +| align="​right"​ | 46645.76
 +| align="​right"​ | 6990528.00
 +| align="​right"​ | 1592.21
 +| align="​right"​ | 225.68
 +| align="​right"​ | 225.68
 +|-
 +|(8,20,1,2)
 +| 100 (99) 99.00%
 +| align="​right"​| 34.69s
 +| 573020.90 (0.00)
 +| 194.87 (154.32)
 +| align="​right"​ | 34692.74
 +| align="​right"​ | 3028.96
 +| align="​right"​ | 194.87
 +| align="​right"​ | 154.32
 +| align="​right"​ | 198205.85
 +| align="​right"​ | 374815.05
 +| align="​right"​ | 0.49
 +| align="​right"​ | 572865.58
 +| align="​right"​ | 198050.03
 +| align="​right"​ | 0.00
 +| align="​right"​ | 213983.03
 +| align="​right"​ | 6990528.00
 +| align="​right"​ | 53879.25
 +| align="​right"​ | 194.00
 +| align="​right"​ | 194.00
 +|-
 +|(2,20,1,2)
 +| 100 (100) 100.00%
 +| align="​right"​| 3.08s
 +| 13109.32 (0.00)
 +| 75.57 (56.05)
 +| align="​right"​ | 3082.10
 +| align="​right"​ | 2982.10
 +| align="​right"​ | 75.57
 +| align="​right"​ | 56.05
 +| align="​right"​ | 4832.29
 +| align="​right"​ | 8277.03
 +| align="​right"​ | 0.90
 +| align="​right"​ | 13052.27
 +| align="​right"​ | 4774.34
 +| align="​right"​ | 0.00
 +| align="​right"​ | 37712.00
 +| align="​right"​ | 6990528.00
 +| align="​right"​ | 309.38
 +| align="​right"​ | 194.00
 +| align="​right"​ | 194.00
 +|-
 +|(2,​100,​1,​2)
 +| 100 (100) 100.00%
 +| align="​right"​| 7.67s
 +| 78569.50 (0.00)
 +| 78.29 (57.01)
 +| align="​right"​ | 7667.78
 +| align="​right"​ | 4665.67
 +| align="​right"​ | 78.29
 +| align="​right"​ | 57.01
 +| align="​right"​ | 28406.49
 +| align="​right"​ | 50163.01
 +| align="​right"​ | 0.98
 +| align="​right"​ | 78511.49
 +| align="​right"​ | 28347.50
 +| align="​right"​ | 0.00
 +| align="​right"​ | 122312.32
 +| align="​right"​ | 6990528.00
 +| align="​right"​ | 24170.40
 +| align="​right"​ | 194.00
 +| align="​right"​ | 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