Concurrency Tool Comparison

Model Description

The Wronglock model contains an error that is caused when two different kinds of threads do not obtain the same lock instance. One type of thread requests a lock on the field object of a class while another type of thread requests a lock on the class containing the field.

Classes:4

SLOC: 38

Summary Results Table

  1. wronglock (10,1)

|- bgcolor=“lightblue”

Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 4999 (4999) 1.00 1.07s 115.71 (0.00) 77.86 (77.17)
(1,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 4999 (4999) 1.00 1.07s 115.71 (0.00) 77.86 (77.17)
JPF Stateless Random Walk 10129 (4842) 0.48 0.03s 2.94 (NA) 0.00 (NA)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (323) 0.32 NA NA (NA) NA (NA)
CalFuzzer 100 (12) 0.12 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 1.47s 1058.00 (NA) 165.00 (165.00)
wronglock (1,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 4998 (4998) 1.00 0.84s 28.04 (0.00) 14.33 (14.16)
JPF Stateless Random Walk 10126 (694) 0.07 0.55s 13.08 (NA) 0.00 (NA)
CHESS 1 (1) 1.00 0.94s 198.00 (9.00) 22.00 (NA)
ConTest 1000 (110) 0.11 NA NA (NA) NA (NA)
CalFuzzer 100 (8) 0.08 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 0.47s 65.00 (NA) 31.00 (31.00)
wronglock (1,10)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 5000 (5000) 1.00 750.10s 11215820.05 (0.00) 59.84 (35.92)
JPF Stateless Random Walk 10128 (2027) 0.20 NA NA (NA) NA (NA)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (243) 0.24 NA NA (NA) NA (NA)
CalFuzzer 100 (11) 0.11 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 0.47s 65.00 (NA) 31.00 (31.00)
wronglock (1,2)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 0.43s 183.05 (0.00) 25.92 (25.67)
JPF Stateless Random Walk 214 (33) 0.15 0.09s 11.09 (NA) 0.00 (NA)
CHESS 1 (1) 1.00 0.50s 3000.00 (100.00) 30.00 (NA)
ConTest 1000 (220) 0.22 NA NA (NA) NA (NA)
CalFuzzer 100 (7) 0.07 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 0.47s 65.00 (NA) 31.00 (31.00)
wronglock (1,20)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 4998 (1000) 0.20 0.92s 41.58 (0.00) 40.58 (40.58)
JPF Stateless Random Walk 10128 (2063) 0.20 0.01s 0.01 (NA) 0.00 (NA)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (220) 0.22 NA NA (NA) NA (NA)
CalFuzzer 100 (11) 0.11 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 0.47s 65.00 (NA) 31.00 (31.00)
wronglock (1,5)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 5.68s 29213.92 (0.00) 46.40 (33.47)
JPF Stateless Random Walk 201 (24) 0.12 0.02s 1.83 (NA) 0.00 (NA)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (230) 0.23 NA NA (NA) NA (NA)
CalFuzzer 100 (8) 0.08 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 0.47s 65.00 (NA) 31.00 (31.00)
wronglock (1,6)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 16.46s 159284.08 (0.00) 53.34 (34.06)
JPF Stateless Random Walk 200 (28) 0.14 NA NA (NA) NA (NA)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (250) 0.25 NA NA (NA) NA (NA)
CalFuzzer 100 (9) 0.09 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 0.47s 65.00 (NA) 31.00 (31.00)
wronglock (10,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 4999 (4999) 1.00 1.07s 115.71 (0.00) 77.86 (77.17)
JPF Stateless Random Walk 10129 (4842) 0.48 0.03s 2.94 (NA) 0.00 (NA)
CHESS 1 (0) 0.00 NA NA (NA) NA (NA)
ConTest 1000 (323) 0.32 NA NA (NA) NA (NA)
CalFuzzer 100 (12) 0.12 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 1.47s 1058.00 (NA) 165.00 (165.00)
wronglock (20,1)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 1.37s 1250.24 (0.00) 146.12 (145.05)
wronglock (5,5)
Tool Trials (successful) Time Transition (paths) Max Depth (error depth)
JPF “Randomized DFS” 100 (100) 1.00 1.52s 6603.42 (0.00) 80.39 (72.36)
JPF Stateless Random Walk 202 (93) 0.46 0.01s 2.13 (NA) 0.00 (NA)
ConTest 1000 (510) 0.51 NA NA (NA) NA (NA)
CalFuzzer 100 (29) 0.29 NA NA (NA) NA (NA)
JPF “Abstraction Guided Refinement” 1 (1) 1.00 0.47s 361.00 (NA) 91.00 (91.00)

Chess

  • ChessBound=2
  • ChessMonitorVolatiles=true
Wronglock Params Tests Found Error Time Taken Steps (Depth)
1,1 9 Yes 0.94 secs 22
1,2 >=100 Yes 0.499 secs 30
1,5 >=668,000 No 3600.331 secs 54
1,6 >=620,000 No 3603.967 secs 62

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.
Wronglock Params Path Error Density
1,1 0.068
1,10 0.200
1,20 0.204
10,1 0.478
1,10 0.200
  • 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
(10,1) 4999 (4999) 100.00% 1.07s 115.71 (0.00) 77.86 (77.17) 1065.53 1065.53 77.86 77.17 95.24 20.47 0.80 37.54 16.54 0.00 13528.85 932096.00 0.00 204.02 204.02
(1,1) 4998 (4998) 100.00% 0.84s 28.04 (0.00) 14.33 (14.16) 835.85 835.85 14.33 14.16 23.85 4.18 1.93 12.87 7.76 0.00 13488.24 932096.00 0.00 168.05 168.05
(1,2) 100 (100) 100.00% 0.43s 183.05 (0.00) 25.92 (25.67) 429.97 429.97 25.92 25.67 103.49 79.56 1.41 156.38 75.92 0.00 21349.76 932096.00 0.00 248.00 248.00
(1,5) 100 (100) 100.00% 5.68s 29213.92 (0.00) 46.40 (33.47) 5683.89 5583.89 46.40 33.47 7557.23 21656.69 0.88 29179.45 7521.89 0.00 54645.12 932096.00 290.14 269.05 273.63
(1,6) 100 (100) 100.00% 16.46s 159284.08 (0.00) 53.34 (34.06) 16464.24 3663.20 53.34 34.06 32999.12 126284.96 0.86 159249.02 32963.22 0.00 91546.24 932096.00 34514.31 270.38 276.64
(20,1) 100 (100) 100.00% 1.37s 1250.24 (0.00) 146.12 (145.05) 1371.52 1371.52 146.12 145.05 375.75 874.49 0.83 1104.19 229.16 0.00 18414.08 6990528.00 0.00 244.00 244.00
(1,10) 5000 (5000) 100.00% 750.10s 11215820.05 (0.00) 59.84 (35.92) 750095.95 4111.95 59.84 35.92 1463916.50 9751903.55 0.80 11215783.12 1463878.78 0.00 294585.37 932096.00 132550.75 195.71 195.93
(1,20) 4998 (1000) 20.01% 0.92s 41.58 (0.00) 40.58 (40.58) 919.08 919.08 40.58 40.58 41.58 0.00 0.00 0.00 0.00 0.00 16141.82 932096.00 0.00 199.19 199.19
(5,5) 100 (100) 100.00% 1.52s 6603.42 (0.00) 80.39 (72.36) 1520.25 1520.25 80.39 72.36 1704.33 4899.09 0.50 6530.06 1630.52 0.00 31015.04 932096.00 0.00 291.57 291.65
(10,1) 4999 (4999) 100.00% 1.07s 115.71 (0.00) 77.86 (77.17) 1065.53 1065.53 77.86 77.17 95.24 20.47 0.80 37.54 16.54 0.00 13528.85 932096.00 0.00 204.02 204.02

ConTest

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

path error density.

Wronglock Params Path Error Density
1,1 0.11
1,2 0.22
1,5 0.23
1,6 0.25
5,5 0.51
1,10 0.243
10,1 0.323
1,20 0.22

CalFuzzer

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

path error density.

Wronglock Params Path Error Density
1,1 0.08
1,2 0.07
1,5 0.08
1,6 0.09
5,5 0.29
1,10 0.11
10,1 0.12
1,20 0.11
vv-lab/wronglock.txt · Last modified: 2015/02/18 23:01 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