Concurrency Tool Comparison

Model Description

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)

Summary Results Table

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)

Chess

  • ChessMonitorVolatiles=true
  • The Bound column specifies the ChessBound parameter
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

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
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
  • 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
(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

ConTest

  • 1000 independent trials
  • The ratio of the error discovery trials over the total number of trials is the

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

CalFuzzer

  • 100 independent trials
  • The ratio of the error discovery trials over the total number of trials is the

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
vv-lab/airline.txt · Last modified: 2015/02/18 22:53 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