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