search
Table of Contents
Model Description
The benchmark contains an atomicity violation with two sequences of operations that need to be protected together but the implementation incorrectly protects the two sequence separately. The input parameters to the benchmark are two different types of threads (twoStagers and readers). The twoStage thread modifies the two separately protected sequences. When the reader thread reads the value of a shared variable between the two accesses by the twoStage thread then a bug is manifested (an exception is raised).
Classes: 5
SLOC: 52
Summary Results Table
| twostage (1,1) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
|---|---|---|---|---|
| JPF “Randomized DFS” | 100 (100) 1.00 | 0.61s | 88.04 (0.00) | 20.18 (18.51) |
| JPF Stateless Random Walk | 10127 (430) 0.04 | 0.02s | 0.94 (NA) | 0.00 (NA) |
| CHESS | 1 (1) 1.00 | 0.94s | 180.00 (9.00) | 20.00 (NA) |
| ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
| JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 3.53s | 30.00 (NA) | 11.00 (11.00) |
| twostage (1,2) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (100) 1.00 | 0.92s | 2286.20 (0.00) | 35.71 (29.10) |
| CHESS | 1 (1) 1.00 | 0.55s | 5800.00 (200.00) | 29.00 (NA) |
| ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
| JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 4.53s | 30.00 (NA) | 11.00 (11.00) |
| twostage (1,3) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (100) 1.00 | 13.16s | 78273.12 (0.00) | 50.59 (34.77) |
| CHESS | 1 (1) 1.00 | 17.38s | 228000.00 (6000.00) | 38.00 (NA) |
| ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
| JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 2.53s | 30.00 (NA) | 11.00 (11.00) |
| twostage (1,5) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (100) 1.00 | 319.01s | 3341784.11 (0.00) | 73.96 (38.09) |
| JPF Stateless Random Walk | 1000 (55) 0.06 | 0.43s | 55.85 (NA) | 0.00 (NA) |
| CHESS | 1 (0) 0.00 | NA | NA (NA) | NA (NA) |
| ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
| JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 2.53s | 30.00 (NA) | 11.00 (11.00) |
| twostage (1,7) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 150 (58) 0.39 | 615.22s | 8442487.19 (0.00) | 77.57 (46.53) |
| twostage (1,8) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 130 (29) 0.22 | 760.96s | 8184336.48 (0.00) | 72.31 (51.24) |
| twostage (10,1) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 4999 (0) 0.00 | NA | NA (NA) | NA (NA) |
| JPF Stateless Random Walk | 10124 (0) 0.00 | NA | NA (NA) | NA (NA) |
| CHESS | 1 (0) 0.00 | NA | NA (NA) | NA (NA) |
| ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
| JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 2.53s | 246.00 (NA) | 29.00 (29.00) |
| twostage (2,1) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (100) 1.00 | 1.07s | 1966.10 (0.00) | 38.46 (30.08) |
| JPF Stateless Random Walk | 1000 (10) 0.01 | 0.30s | 30.20 (NA) | 0.00 (NA) |
| CHESS | 1 (1) 1.00 | 0.52s | 5800.00 (200.00) | 29.00 (NA) |
| ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
| JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 3.53s | 46.00 (NA) | 13.00 (13.00) |
| twostage (2,2) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (100) 1.00 | 2.41s | 10223.50 (0.00) | 45.72 (36.07) |
| CHESS | 1 (1) 1.00 | 17.44s | 228000.00 (6000.00) | 38.00 (NA) |
| ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
| JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 3.53s | 46.00 (NA) | 13.00 (13.00) |
| twostage (2,5) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (100) 1.00 | 518.46s | 8968986.03 (0.00) | 81.30 (46.71) |
| CHESS | 1 (0) 0.00 | NA | NA (NA) | NA (NA) |
| ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
| JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 2.53s | 46.00 (NA) | 13.00 (13.00) |
| twostage (2,6) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 125 (36) 0.29 | 1666.94s | 22273647.86 (0.00) | 90.06 (50.17) |
| twostage (3,1) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (100) 1.00 | 10.14s | 56717.85 (0.00) | 53.76 (40.57) |
| JPF Stateless Random Walk | 1000 (1) 0.00 | 0.59s | 49.00 (NA) | 0.00 (NA) |
| CHESS | 1 (1) 1.00 | 16.64s | 228000.00 (6000.00) | 38.00 (NA) |
| ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
| JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 2.53s | 64.00 (NA) | 15.00 (15.00) |
| twostage (3,5) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 106 (40) 0.38 | 1968.26s | 32880318.60 (0.00) | 90.78 (53.70) |
| twostage (4,1) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (100) 1.00 | 30.84s | 288171.90 (0.00) | 68.06 (50.25) |
| JPF Stateless Random Walk | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
| CHESS | 1 (1) 1.00 | 754.66s | 9400000.00 (200000.00) | 47.00 (NA) |
| ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
| JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 2.53s | 84.00 (NA) | 17.00 (17.00) |
| twostage (4,4) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 114 (27) 0.24 | 2106.31s | 29409673.52 (0.00) | 94.67 (59.85) |
| twostage (5,1) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 100 (100) 1.00 | 321.14s | 3272083.66 (0.00) | 81.82 (59.83) |
| CHESS | 1 (0) 0.00 | NA | NA (NA) | NA (NA) |
| ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
| JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 2.53s | 106.00 (NA) | 19.00 (19.00) |
| twostage (5,2) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 97 (97) 1.00 | 459.54s | 7977266.73 (0.00) | 82.94 (59.40) |
| twostage (5,3) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 117 (33) 0.28 | 1751.81s | 27545439.15 (0.00) | 94.94 (63.45) |
| twostage (6,1) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 5000 (5000) 1.00 | 464.28s | 7882244.02 (0.00) | 83.00 (60.13) |
| JPF Stateless Random Walk | 10128 (2) 0.00 | NA | NA (NA) | NA (NA) |
| CHESS | 1 (0) 0.00 | NA | NA (NA) | NA (NA) |
| ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
| JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 2.53s | 130.00 (NA) | 21.00 (21.00) |
| twostage (6,2) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 130 (37) 0.28 | 1616.85s | 20977457.46 (0.00) | 94.78 (65.76) |
| twostage (7,1) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 5000 (2299) 0.46 | 1815.53s | 27704831.56 (0.00) | 94.96 (67.75) |
| JPF Stateless Random Walk | 10128 (0) 0.00 | NA | NA (NA) | NA (NA) |
| CHESS | 1 (0) 0.00 | NA | NA (NA) | NA (NA) |
| ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
| JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 2.53s | 156.00 (NA) | 23.00 (23.00) |
| twostage (8,1) | ||||
| Tool | Trials (successful) | Time | Transition (paths) | Max Depth (error depth) |
| JPF “Randomized DFS” | 4999 (126) 0.03 | 2155.76s | 32969192.09 (0.00) | 105.46 (73.40) |
| JPF Stateless Random Walk | 10200 (0) 0.00 | NA | NA (NA) | NA (NA) |
| CHESS | 1 (0) 0.00 | NA | NA (NA) | NA (NA) |
| ConTest | 1000 (0) 0.00 | NA | NA (NA) | NA (NA) |
| JPF “Abstraction Guided Refinement” | 1 (1) 1.00 | 2.53s | 184.00 (NA) | 25.00 (25.00) |
Chess
- ChessBound=2
- ChessMonitorVolatiles=false
| TwoStage Params | Tests | Found Error | Time Taken | Steps (Depth) |
|---|---|---|---|---|
| 1,1 | 9 | Yes | 0.94 secs | 20 |
| 1,2 | >=200 | Yes | 0.546 secs | 29 |
| 2,1 | >=200 | Yes | 0.515 secs | 29 |
| 2,2 | >=6000 | Yes | 17.441 secs | 38 |
| 1,3 | >=6000 | Yes | 17.378 secs | 38 |
| 3,1 | >=6000 | Yes | 16.645 secs | 38 |
| 4,1 | >=200,000 | Yes | 754.655 secs | 47 |
| 1,5 | >=1,059,000 | No | 3602.282 secs | 56 |
| 5,1 | >=1,064,000 | No | 3602.422 secs | 56 |
| 6,1 | >=970,000 | No | 3604.022 secs | 56 |
| 2,5 | >=969,000 | No | 3600.35 secs | 65 |
| 2,5 | >=969,000 | No | 3600.35 secs | 65 |
| 7,1 | >=879,000 | No | 3601.205 secs | 74 |
| 8,1 | >=821,000 | No | 3602.135 secs | 83 |
| 10,1 | >=714,000 | No | 3600.206 secs | 83 |
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.
| TwoStage Params | Path Error Density |
|---|---|
| 1,1 | 0.043 |
| 2,2 | 0.022 |
| 2,5 | 0.028 |
| 6,1 | 0.0002 |
| 7,1 | 0.0 |
| 8,1 | 0.0 |
| 10,1 | 0.0 |
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 | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| (6,1) | 5000 (5000) 100.00% | 464.28s | 7882244.02 (0.00) | 83.00 (60.13) | 464282.52 | 5068.92 | 83.00 | 60.13 | 1586963.57 | 6295280.44 | 1.00 | 7882182.88 | 1586901.44 | 0.00 | 392921.75 | 932096.00 | 185330.38 | 193.00 | 193.00 | |
| (6,2) | 130 (37) 28.46% | 1616.85s | 20977457.46 (0.00) | 94.78 (65.76) | 1616853.00 | 4244.54 | 94.78 | 65.76 | 4040281.35 | 16937176.11 | 1.00 | 20977390.70 | 4040213.59 | 0.00 | 2413953.73 | 6990528.00 | 1101639.38 | 197.03 | 197.03 | |
| (7,1) | 5000 (2299) 45.98% | 1815.53s | 27704831.56 (0.00) | 94.96 (67.75) | 1815534.19 | 4892.96 | 94.96 | 67.75 | 5278666.49 | 22426165.07 | 1.00 | 27704762.81 | 5278596.74 | 0.00 | 477712.12 | 932096.00 | 202529.28 | 197.01 | 197.01 | |
| (1,1) | 100 (100) 100.00% | 0.61s | 88.04 (0.00) | 20.18 (18.51) | 612.70 | 612.70 | 20.18 | 18.51 | 56.67 | 31.37 | 1.04 | 68.53 | 36.18 | 0.00 | 15553.28 | 6990528.00 | 0.00 | 173.08 | 173.08 | |
| (1,2) | 100 (100) 100.00% | 0.92s | 2286.20 (0.00) | 35.71 (29.10) | 918.46 | 918.46 | 35.71 | 29.10 | 817.13 | 1469.07 | 0.93 | 2256.10 | 786.19 | 0.00 | 26549.76 | 932096.00 | 0.00 | 251.19 | 251.91 | |
| (1,3) | 100 (100) 100.00% | 13.16s | 78273.12 (0.00) | 50.59 (34.77) | 13157.28 | 4255.89 | 50.59 | 34.77 | 25204.08 | 53069.04 | 0.99 | 78237.35 | 25167.32 | 0.00 | 79715.20 | 932096.00 | 27159.95 | 272.12 | 272.68 | |
| (1,5) | 100 (100) 100.00% | 319.01s | 3341784.11 (0.00) | 73.96 (38.09) | 319014.62 | 4503.47 | 73.96 | 38.09 | 683349.85 | 2658434.26 | 0.92 | 3341745.02 | 683309.84 | 0.00 | 157665.92 | 932096.00 | 37416.00 | 278.52 | 279.90 | |
| (1,7) | 150 (58) 38.67% | 615.22s | 8442487.19 (0.00) | 77.57 (46.53) | 615215.91 | 3348.79 | 77.57 | 46.53 | 1559333.97 | 6883153.22 | 0.83 | 8442439.66 | 1559285.60 | 0.00 | 1366030.34 | 6990528.00 | 525682.10 | 197.71 | 197.71 | |
| (1,8) | 130 (29) 22.31% | 760.96s | 8184336.48 (0.00) | 72.31 (51.24) | 760962.59 | 3539.07 | 72.31 | 51.24 | 1453206.17 | 6731130.31 | 0.66 | 8184284.24 | 1453153.28 | 0.00 | 934430.90 | 6990528.00 | 446142.62 | 200.10 | 200.10 | |
| (8,1) | 4999 (126) 2.52% | 2155.76s | 32969192.09 (0.00) | 105.46 (73.40) | 2155760.02 | 4799.94 | 105.46 | 73.40 | 6480559.25 | 26488632.84 | 1.00 | 32969117.69 | 6480483.85 | 0.00 | 505722.92 | 932096.00 | 223251.82 | 201.00 | 201.00 | |
| (2,1) | 100 (100) 100.00% | 1.07s | 1966.10 (0.00) | 38.46 (30.08) | 1067.09 | 1067.09 | 38.46 | 30.08 | 746.72 | 1219.38 | 0.99 | 1935.02 | 715.23 | 0.00 | 25803.52 | 932096.00 | 0.00 | 244.46 | 249.10 | |
| (2,2) | 100 (100) 100.00% | 2.41s | 10223.50 (0.00) | 45.72 (36.07) | 2406.28 | 2406.28 | 45.72 | 36.07 | 3300.70 | 6922.80 | 0.99 | 10186.43 | 3262.64 | 0.00 | 31480.96 | 6990528.00 | 0.00 | 181.12 | 181.12 | |
| (2,5) | 100 (100) 100.00% | 518.46s | 8968986.03 (0.00) | 81.30 (46.71) | 518462.59 | 4775.78 | 81.30 | 46.71 | 1759759.44 | 7209226.59 | 0.97 | 8968938.32 | 1759710.76 | 0.00 | 1726579.20 | 6990528.00 | 635963.42 | 194.39 | 194.39 | |
| (2,6) | 125 (36) 28.80% | 1666.94s | 22273647.86 (0.00) | 90.06 (50.17) | 1666940.14 | 3480.08 | 90.06 | 50.17 | 4105668.44 | 18167979.42 | 0.94 | 22273596.69 | 4105616.33 | 0.00 | 2283043.56 | 6990528.00 | 1147659.22 | 198.64 | 198.64 | |
| (3,1) | 100 (100) 100.00% | 10.14s | 56717.85 (0.00) | 53.76 (40.57) | 10142.53 | 4741.55 | 53.76 | 40.57 | 19029.75 | 37688.10 | 1.00 | 56676.28 | 18987.84 | 0.00 | 72305.28 | 932096.00 | 17963.74 | 262.42 | 267.70 | |
| (3,5) | 106 (40) 37.74% | 1968.26s | 32880318.60 (0.00) | 90.78 (53.70) | 1968262.65 | 4380.48 | 90.78 | 53.70 | 6079980.10 | 26800338.50 | 0.90 | 32880263.90 | 6079924.50 | 0.00 | 2392500.80 | 6990528.00 | 1167632.68 | 198.28 | 198.28 | |
| (10,1) | 4999 (0) 0.00% | |||||||||||||||||||
| (4,1) | 100 (100) 100.00% | 30.84s | 288171.90 (0.00) | 68.06 (50.25) | 30844.89 | 4437.01 | 68.06 | 50.25 | 74878.02 | 213293.88 | 1.00 | 288120.65 | 74826.56 | 0.00 | 117380.48 | 932096.00 | 49747.98 | 264.73 | 271.05 | |
| (4,4) | 114 (27) 23.68% | 2106.31s | 29409673.52 (0.00) | 94.67 (59.85) | 2106310.30 | 3547.56 | 94.67 | 59.85 | 5589241.56 | 23820431.96 | 1.00 | 29409612.67 | 5589179.70 | 0.00 | 2646885.93 | 6990528.00 | 1270640.63 | 197.26 | 197.26 | |
| (5,1) | 100 (100) 100.00% | 321.14s | 3272083.66 (0.00) | 81.82 (59.83) | 321144.06 | 4221.71 | 81.82 | 59.83 | 697572.24 | 2574511.42 | 1.00 | 3272022.83 | 697511.08 | 0.00 | 177150.08 | 932096.00 | 40599.68 | 270.29 | 275.65 | |
| (5,2) | 97 (97) 100.00% | 459.54s | 7977266.73 (0.00) | 82.94 (59.40) | 459535.48 | 4536.60 | 82.94 | 59.40 | 1601368.30 | 6375898.43 | 1.00 | 7977206.33 | 1601306.90 | 0.00 | 1789834.56 | 6990528.00 | 663180.38 | 193.01 | 193.01 | |
| (5,3) | 117 (33) 28.21% | 1751.81s | 27545439.15 (0.00) | 94.94 (63.45) | 1751814.09 | 4889.55 | 94.94 | 63.45 | 5290511.58 | 22254927.58 | 1.00 | 27545374.70 | 5290446.12 | 0.00 | 2647683.88 | 6990528.00 | 1311998.91 | 197.24 | 197.24 |
ConTest
- 1000 independent trials
- The ratio of the error discovery trials over the total number of trials is the
path error density.
| TwoStage Params | Path Error Density |
|---|---|
| 1,1 | 0.000 |
| 2,1 | 0.000 |
| 3,1 | 0.000 |
| 4,1 | 0.000 |
| 5,1 | 0.000 |
| 6,1 | 0.000 |
| 1,5 | 0.000 |
| 1,2 | 0.000 |
| 2,2 | 0.000 |
| 1,3 | 0.000 |
| 2,5 | 0.000 |
| 7,1 | 0.000 |
| 8,1 | 0.000 |
| 10,1 | 0.000 |
CalFuzzer
Not Applicable. The initial dynamic analysis does not find any input target locations.
