[[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
|}