search
Table of Contents
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
|- 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 |
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).
| 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 |
