The benchmark contains a data race. As the number of threads are created the value of a global variable is updated. An incorrect assumption on atomicity allows more threads to be created leading to a data inconsistency. The two parameters to the airline model are: ticketsIssued and cushion. The minimum depth of the error is pushed deeper in the execution trace when we increase the value of the cushion and keep the total number of threads, ticketsIssued, constant.
Classes: 2
SLOC: 31
Parameters: (#ticketsIssued, cushion)
airline (20,1) | ||||
Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
---|---|---|---|---|
JPF “Randomized DFS” | 4996 (0) 0.00 | NA | NA (NA) | NA (NA) |
JPF Stateless Random Walk | 11125 (1) 0.00 | NA | NA (NA) | NA (NA) |
ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
CalFuzzer | 100 (0) 0.00 | NA | NA (NA) | NA (NA) |
JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 7.46s | 3609.00 (NA) | 95.00 (95.00) |
airline (20,2) | ||||
Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
JPF “Randomized DFS” | 4999 (6) 0.00 | 562.24s | 8577017.83 (0.00) | 122.17 (120.00) |
JPF Stateless Random Walk | 14998 (0) 0.00 | NA | NA (NA) | NA (NA) |
ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
CalFuzzer | 100 (0) 0.00 | NA | NA (NA) | NA (NA) |
JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 7.46s | 3279.00 (NA) | 78.00 (78.00) |
airline (20,3) | ||||
Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
JPF “Randomized DFS” | 4992 (24) 0.00 | 375.78s | 5905884.67 (0.00) | 121.75 (119.75) |
JPF Stateless Random Walk | 11132 (19) 0.00 | NA | NA (NA) | NA (NA) |
ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
CalFuzzer | 100 (0) 0.00 | NA | NA (NA) | NA (NA) |
JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 7.46s | 3210.00 (NA) | 75.00 (75.00) |
airline (20,4) | ||||
Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
JPF “Randomized DFS” | 5000 (116) 0.02 | 461.52s | 6711300.33 (0.00) | 121.91 (119.87) |
JPF Stateless Random Walk | 11129 (70) 0.01 | NA | NA (NA) | NA (NA) |
ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
CalFuzzer | 100 (0) 0.00 | NA | NA (NA) | NA (NA) |
JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 7.46s | 3134.00 (NA) | 72.00 (72.00) |
airline (20,5) | ||||
Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
JPF “Randomized DFS” | 5000 (360) 0.07 | 448.37s | 6595025.32 (0.00) | 121.91 (119.97) |
JPF Stateless Random Walk | 11140 (197) 0.02 | NA | NA (NA) | NA (NA) |
ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
CalFuzzer | 100 (0) 0.00 | NA | NA (NA) | NA (NA) |
JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 5.46s | 3042.00 (NA) | 69.00 (69.00) |
airline (20,6) | ||||
Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
JPF “Randomized DFS” | 4999 (876) 0.18 | 464.12s | 6820760.72 (0.00) | 121.75 (119.74) |
JPF Stateless Random Walk | 11159 (405) 0.04 | NA | NA (NA) | NA (NA) |
CalFuzzer | 100 (0) 0.00 | NA | NA (NA) | NA (NA) |
JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 5.46s | 2935.00 (NA) | 66.00 (66.00) |
airline (20,7) | ||||
Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
JPF “Randomized DFS” | 5000 (1665) 0.33 | 300.64s | 4332959.57 (0.00) | 121.48 (119.28) |
JPF Stateless Random Walk | 11206 (790) 0.07 | NA | NA (NA) | NA (NA) |
CalFuzzer | 100 (0) 0.00 | NA | NA (NA) | NA (NA) |
JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 5.46s | 2680.00 (NA) | 60.00 (60.00) |
airline (20,8) | ||||
Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
JPF “Randomized DFS” | 5000 (2507) 0.50 | 285.85s | 4111966.14 (0.00) | 121.07 (118.62) |
JPF Stateless Random Walk | 10123 (696) 0.07 | NA | NA (NA) | NA (NA) |
CalFuzzer | 100 (0) 0.00 | NA | NA (NA) | NA (NA) |
JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 5.46s | 2680.00 (NA) | 60.00 (60.00) |
airline (4,1) | ||||
Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
JPF “Randomized DFS” | 200 (200) 1.00 | 0.81s | 5776.74 (0.00) | 14.28 (13.23) |
JPF Stateless Random Walk | 1011 (98) 0.10 | NA | NA (NA) | NA (NA) |
CalFuzzer | 100 (0) 0.00 | NA | NA (NA) | NA (NA) |
JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 3.46s | 61.00 (NA) | 17.00 (17.00) |
airline (4,2) | ||||
Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
JPF “Randomized DFS” | 200 (200) 1.00 | 0.25s | 655.86 (0.00) | 13.75 (12.59) |
JPF Stateless Random Walk | 1021 (433) 0.42 | NA | NA (NA) | NA (NA) |
CalFuzzer | 100 (0) 0.00 | NA | NA (NA) | NA (NA) |
JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 3.46s | 46.00 (NA) | 14.00 (14.00) |
airline (5,1) | ||||
Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
JPF “Randomized DFS” | 200 (200) 1.00 | 58.19s | 670929.50 (0.00) | 25.28 (22.17) |
JPF Stateless Random Walk | 1021 (111) 0.11 | NA | NA (NA) | NA (NA) |
CalFuzzer | 100 (0) 0.00 | NA | NA (NA) | NA (NA) |
JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 3.46s | 98.00 (NA) | 21.00 (21.00) |
airline (5,3) | ||||
Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
JPF “Randomized DFS” | 200 (200) 1.00 | 0.31s | 689.12 (0.00) | 16.77 (15.96) |
JPF Stateless Random Walk | 1098 (725) 0.66 | NA | NA (NA) | NA (NA) |
CalFuzzer | 100 (0) 0.00 | NA | NA (NA) | NA (NA) |
JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 3.46s | 65.00 (NA) | 15.00 (15.00) |
airline (6,1) | ||||
Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
JPF “Randomized DFS” | 100 (100) 1.00 | 394.33s | 8876025.11 (0.00) | 37.99 (36.33) |
JPF Stateless Random Walk | 10129 (29) 0.00 | NA | NA (NA) | NA (NA) |
ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
CalFuzzer | 100 (0) 0.00 | NA | NA (NA) | NA (NA) |
JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 3.46s | 163.00 (NA) | 28.00 (28.00) |
airline (6,2) | ||||
Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
JPF “Randomized DFS” | 100 (100) 1.00 | 54.62s | 1166530.67 (0.00) | 38.01 (35.77) |
JPF Stateless Random Walk | 10129 (306) 0.03 | NA | NA (NA) | NA (NA) |
ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
CalFuzzer | 100 (0) 0.00 | NA | NA (NA) | NA (NA) |
JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 3.46s | 127.00 (NA) | 22.00 (22.00) |
Airline Params | Bound | Tests | Found Error | Time Taken | Steps (Depth) |
---|---|---|---|---|---|
4,1 | 2 | 45,618 | No | 231.240 secs | 114 |
4,1 | 3 | >=394,000 | Yes | 1983.522 secs | 114 |
4,2 | 2 | >=13,000 | Yes | 67.533 secs | |
5,1 | 2 | 115,648 | No | 672.582 secs | |
5,1 | 3 | >=638,000 | No | 3604.559 secs | |
5,1 | 4 | >=654,000 | No | 3602.187 secs | |
5,3 | 2 | 115,694 | No | 640.290 secs | |
5,3 | 3 | >=655,000 | No | 3647.179 secs | |
path error density.
Parameters | Path Error Density |
---|---|
6,1 | 0.003 |
6,2 | 0.030 |
20,1 | 0.0 |
20,2 | 0.0 |
20,8 | 0.069 |
20,2 | 0.000 |
20,3 | 0.0 |
20,4 | 0.0002 |
20,5 | 0.002 |
20,6 | 0.008 |
20,7 | 0.023 |
20,8 | 0.067 |
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 |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
(4,1) | 200 (200) 100.00% | 0.81s | 5776.74 (0.00) | 14.28 (13.23) | 809.18 | 809.18 | 14.28 | 13.23 | 1564.63 | 4212.11 | 1.19 | 5763.02 | 1549.78 | 0.00 | 15553.28 | 466048.00 | 0.00 | 126.00 | 126.00 |
(4,2) | 200 (200) 100.00% | 0.25s | 655.86 (0.00) | 13.75 (12.59) | 248.02 | 248.02 | 13.75 | 12.59 | 224.00 | 431.86 | 0.65 | 642.76 | 210.31 | 0.00 | 10607.04 | 466048.00 | 0.00 | 125.67 | 125.67 |
(5,1) | 200 (200) 100.00% | 58.19s | 670929.49 (0.00) | 25.27 (22.17) | 58193.73 | 3638.97 | 25.27 | 22.17 | 162604.83 | 508324.66 | 2.25 | 670906.62 | 162579.92 | 0.00 | 86600.00 | 647806.72 | 25705.27 | 185.53 | 185.81 |
(5,3) | 200 (200) 100.00% | 0.31s | 689.12 (0.00) | 16.77 (15.96) | 305.05 | 305.05 | 16.77 | 15.96 | 217.67 | 471.45 | 0.41 | 672.66 | 200.84 | 0.00 | 12360.00 | 466048.00 | 0.00 | 135.50 | 135.50 |
(20,1) | 4996 (0) 0.00% | ||||||||||||||||||
(20,2) | 4999 (6) 0.12% | 562.24s | 8577017.83 (0.00) | 122.17 (120.00) | 562241.83 | 3794.33 | 122.17 | 120.00 | 1550536.17 | 7026481.67 | 5.17 | 8576896.83 | 1550410.50 | 0.00 | 290080.00 | 932096.00 | 170562.17 | 241.00 | 241.00 |
(20,3) | 4992 (24) 0.48% | 375.78s | 5905884.67 (0.00) | 121.75 (119.75) | 375779.33 | 4861.17 | 121.75 | 119.75 | 1036133.12 | 4869751.54 | 4.54 | 5905763.92 | 1036008.00 | 0.00 | 291136.00 | 932096.00 | 144767.75 | 241.00 | 241.00 |
(20,4) | 5000 (116) 2.32% | 461.52s | 6711300.33 (0.00) | 121.91 (119.87) | 461516.77 | 4707.47 | 121.91 | 119.87 | 1153254.41 | 5558045.91 | 4.46 | 6711179.46 | 1153129.28 | 0.00 | 278695.17 | 932096.00 | 124799.82 | 241.00 | 241.00 |
(20,5) | 5000 (360) 7.20% | 448.37s | 6595025.33 (0.00) | 121.91 (119.97) | 448365.35 | 4467.86 | 121.91 | 119.97 | 1147611.88 | 5447413.44 | 4.42 | 6594904.36 | 1147486.72 | 0.00 | 277988.27 | 932096.00 | 115750.97 | 241.00 | 241.00 |
(20,6) | 4999 (876) 17.52% | 464.12s | 6820760.72 (0.00) | 121.75 (119.74) | 464123.49 | 4134.85 | 121.75 | 119.74 | 1171490.87 | 5649269.84 | 4.13 | 6820639.98 | 1171366.22 | 0.00 | 258675.51 | 932096.00 | 101841.83 | 241.00 | 241.00 |
(20,7) | 5000 (1665) 33.30% | 300.64s | 4332959.57 (0.00) | 121.48 (119.28) | 300641.40 | 4031.49 | 121.48 | 119.28 | 748081.85 | 3584877.72 | 3.73 | 4332839.30 | 747958.06 | 0.00 | 227616.67 | 932096.00 | 95063.95 | 240.99 | 240.99 |
(20,8) | 5000 (2507) 50.14% | 285.85s | 4111966.14 (0.00) | 121.07 (118.62) | 285851.37 | 3876.37 | 121.07 | 118.62 | 711998.03 | 3399968.11 | 3.41 | 4111846.51 | 711875.19 | 0.00 | 209404.25 | 932096.00 | 89145.86 | 240.89 | 240.89 |
(6,1) | 100 (100) 100.00% | 394.33s | 8876025.11 (0.00) | 37.99 (36.33) | 394325.24 | 4607.12 | 37.99 | 36.33 | 1618914.82 | 7257110.29 | 5.10 | 8875987.78 | 1618872.63 | 0.00 | 1310046.72 | 6990528.00 | 580593.25 | 185.00 | 185.00 |
(6,2) | 100 (100) 100.00% | 54.62s | 1166530.67 (0.00) | 38.01 (35.77) | 54619.07 | 3717.12 | 38.01 | 35.77 | 226845.59 | 939685.08 | 3.73 | 1166493.90 | 226805.31 | 0.00 | 317019.52 | 6990528.00 | 116839.71 | 185.00 | 185.00 |
path error density.
Airline Params | Path Error Density |
---|---|
6,1 | 0.00 |
6,2 | 0.00 |
20,1 | 0.00 |
20,2 | 0.00 |
20,3 | 0.00 |
20,4 | 0.00 |
20,5 | 0.00 |
path error density.
Airline Params | Path Error Density |
---|---|
4,1 | 0.00 |
4,2 | 0.00 |
5,1 | 0.00 |
5,3 | 0.00 |
6,1 | 0.00 |
6,2 | 0.00 |
20,1 | 0.00 |
20,2 | 0.00 |
20,3 | 0.00 |
20,4 | 0.00 |
20,5 | 0.00 |
20,6 | 0.00 |
20,7 | 0.00 |
20,8 | 0.00 |