[[Concurrency Tool Comparison]]

== Model Description == 

A race condition in producer and consumer model. 

Classes: 8

SLOC: 87

Parameters: (#prod, #cons, #items)

== Summary Results Table ==

{| align=center | border=1
|- bgcolor="white" |
| colspan=5 align="center" | producerconsumer (1,10,4)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 115 (84) 0.73
| align="right"| 86.11s
| 963174.08 (0.00)
| 121.87 (116.52)
|-
| JPF Stateless Random Walk
| 10125 (5434) 0.54
| align="right"| 1.22s
| 116.26 (NA)
| 0.00 (NA)
|- bgcolor="white" |
| colspan=5 align="center" | producerconsumer (1,12,4)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 135 (93) 0.69
| align="right"| 146.54s
| 1677307.59 (0.00)
| 133.19 (128.74)
|-
| JPF Stateless Random Walk
| 10125 (5405) 0.53
| align="right"| 1.26s
| 126.19 (NA)
| 0.00 (NA)
|- bgcolor="white" |
| colspan=5 align="center" | producerconsumer (1,16,4)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 4999 (2736) 0.55
| align="right"| 25.65s
| 283379.04 (0.00)
| 146.74 (145.98)
|-
| JPF Stateless Random Walk
| 10113 (5380) 0.53
| align="right"| 1.18s
| 146.01 (NA)
| 0.00 (NA)
|- bgcolor="white" |
| colspan=5 align="center" | producerconsumer (1,8,4)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 115 (111) 0.97
| align="right"| 94.91s
| 1300588.95 (0.00)
| 113.86 (107.14)
|-
| JPF Stateless Random Walk
| 10122 (5389) 0.53
| align="right"| 1.10s
| 105.43 (NA)
| 0.00 (NA)
|- bgcolor="white" |
| colspan=5 align="center" | producerconsumer (2,2,4)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 0.83s
| 120.42 (0.00)
| 99.09 (98.25)
|-
| JPF Stateless Random Walk
| 10124 (7760) 0.77
| align="right"| 1.11s
| 98.42 (NA)
| 0.00 (NA)
|- bgcolor="white" |
| colspan=5 align="center" | producerconsumer (2,4,4)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 0.87s
| 120.46 (0.00)
| 110.75 (110.65)
|-
| JPF Stateless Random Walk
| 10126 (9680) 0.96
| align="right"| 1.13s
| 111.14 (NA)
| 0.00 (NA)
|- bgcolor="white" |
| colspan=5 align="center" | producerconsumer (2,8,4)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 0.99s
| 593.74 (0.00)
| 135.70 (135.49)
|-
| JPF Stateless Random Walk
| 10126 (9799) 0.97
| align="right"| 1.11s
| 134.56 (NA)
| 0.00 (NA)
|- bgcolor="white" |
| colspan=5 align="center" | producerconsumer (7,10,4)
|- bgcolor="lightblue"
! Tool
! Trials (successful)
! Time
! Transition (paths)
! Max Depth (error depth)
|-
| JPF "Randomized DFS"
| 100 (100) 1.00
| align="right"| 1.22s
| 370.09 (0.00)
| 369.09 (369.09)
|}
==Java Pathfinder==
===Stateless Random Walk===

{| align=center | border=1 | -bgcolor=grey
! Parameters !! Path Error Density
|-
| 1,8,4 || 0.532
|- 
| 1,10,4 || 0.537
|-
| 1,12,4 || 0.534
|-
| 1,16,4 || 0.531
|-
| 2,2,4 || 0.767
|-
| 2,2,4 || 0.956
|-
| 2,8,4 || 0.967
|}

===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

|-
|(1,12,4)
| 135 (93) 68.89%
| align="right"| 146.54s
| 1677307.59 (0.00)
| 133.19 (128.74)
| align="right" | 146535.80
| align="right" | 1531.52
| align="right" | 133.19
| align="right" | 128.74
| align="right" | 235782.88
| align="right" | 1441524.71
| align="right" | 1.20
| align="right" | 1677177.85
| align="right" | 235652.94
| align="right" | 0.00
| align="right" | 306280.60
| align="right" | 6990528.00
| align="right" | 141235.20
| align="right" | 237.00
| align="right" | 237.00
|-
|(2,8,4)
| 100 (100) 100.00%
| align="right"| 0.99s
| 593.74 (0.00)
| 135.70 (135.49)
| align="right" | 985.94
| align="right" | 985.94
| align="right" | 135.70
| align="right" | 135.49
| align="right" | 260.76
| align="right" | 332.98
| align="right" | 1.02
| align="right" | 457.25
| align="right" | 124.25
| align="right" | 0.00
| align="right" | 17381.76
| align="right" | 6990528.00
| align="right" | 0.00
| align="right" | 225.07
| align="right" | 225.07
|-
|(7,10,4)
| 100 (100) 100.00%
| align="right"| 1.22s
| 370.09 (0.00)
| 369.09 (369.09)
| align="right" | 1217.91
| align="right" | 1217.91
| align="right" | 369.09
| align="right" | 369.09
| align="right" | 370.09
| align="right" | 0.00
| align="right" | 1.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 0.00
| align="right" | 17490.56
| align="right" | 6990528.00
| align="right" | 0.00
| align="right" | 253.02
| align="right" | 261.46
|-
|(2,2,4)
| 100 (100) 100.00%
| align="right"| 0.83s
| 120.42 (0.00)
| 99.09 (98.25)
| align="right" | 831.93
| align="right" | 831.93
| align="right" | 99.09
| align="right" | 98.25
| align="right" | 111.74
| align="right" | 8.68
| align="right" | 1.20
| align="right" | 21.17
| align="right" | 12.28
| align="right" | 0.00
| align="right" | 16512.00
| align="right" | 6990528.00
| align="right" | 0.00
| align="right" | 200.93
| align="right" | 200.93
|-
|(2,4,4)
| 100 (100) 100.00%
| align="right"| 0.87s
| 120.46 (0.00)
| 110.75 (110.65)
| align="right" | 865.74
| align="right" | 865.74
| align="right" | 110.75
| align="right" | 110.65
| align="right" | 115.66
| align="right" | 4.80
| align="right" | 1.03
| align="right" | 8.81
| align="right" | 3.98
| align="right" | 0.00
| align="right" | 16368.00
| align="right" | 6990528.00
| align="right" | 0.00
| align="right" | 209.02
| align="right" | 209.02
|-
|(1,8,4)
| 115 (111) 96.52%
| align="right"| 94.91s
| 1300588.95 (0.00)
| 113.86 (107.14)
| align="right" | 94906.75
| align="right" | 3281.18
| align="right" | 113.86
| align="right" | 107.14
| align="right" | 200326.51
| align="right" | 1100262.43
| align="right" | 1.49
| align="right" | 1300480.80
| align="right" | 200217.88
| align="right" | 0.00
| align="right" | 323747.17
| align="right" | 6990528.00
| align="right" | 108138.57
| align="right" | 221.00
| align="right" | 221.00
|-
|(1,16,4)
| 4999 (2736) 54.73%
| align="right"| 25.65s
| 283379.04 (0.00)
| 146.74 (145.98)
| align="right" | 25645.56
| align="right" | 1081.17
| align="right" | 146.74
| align="right" | 145.98
| align="right" | 38927.38
| align="right" | 244451.65
| align="right" | 1.03
| align="right" | 283232.06
| align="right" | 38780.38
| align="right" | 0.00
| align="right" | 24845.89
| align="right" | 932096.00
| align="right" | 4041.29
| align="right" | 253.00
| align="right" | 253.00
|-
|(1,10,4)
| 115 (84) 73.04%
| align="right"| 86.11s
| 963174.08 (0.00)
| 121.87 (116.52)
| align="right" | 86108.83
| align="right" | 2191.33
| align="right" | 121.87
| align="right" | 116.52
| align="right" | 138683.65
| align="right" | 824490.43
| align="right" | 1.30
| align="right" | 963056.56
| align="right" | 138565.83
| align="right" | 0.00
| align="right" | 209030.10
| align="right" | 6990528.00
| align="right" | 78466.30
| align="right" | 229.00
| align="right" | 229.00
|}