| * satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 version 3.0 results * Timeout: 1800s Memory limit: unlimitedkb Fri Jan 27 17:19:09 2012 |
|||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Benchmark | Broadcast assignment operations executed | Invalid states requiring more than 1 passive thread | Iterations | Local predicates | Max number of slots used | Mixed predicates | Non-broadcast assignment operations executed | Result | Shared predicates | Spurious assignment transitions requiring more than 1 passive thread | Spurious guard transitions requiring more than 1 passive thread | Time abstractor | Time model checker | Time refiner | Time simulator | Time spent in broadcast assignment operations | Time spent in non-broadcast assignment operations | Total transition refinements | Transition refinements | commandline | date | exitcode | expected | maxmem | user | usertime | wallclock |
| regression/symmetry_aware_cav12threader/01_spin2003/test | 0 | 0 | 2 | 0 | 0 | 0 | 42 | SUCCESSFUL | 3 | 0 | 0 | 0.002 | 0.069 | 0.006 | 0 | 0 | 0.000239 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/01_spin2003/test.bin | Thu Dec 8 21:20:57 GMT 2011 | 0 | valid | 45952kb | alexk | 0.08 | 0:00.08 |
| regression/symmetry_aware_cav12threader/02_dekker/test | 0 | 0 | 2 | 0 | 0 | 0 | 133 | SUCCESSFUL | 5 | 0 | 0 | 0.005 | 0.08 | 0.008 | 0.001 | 0 | 0.000622 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/02_dekker/test.bin | Thu Dec 8 21:20:58 GMT 2011 | 0 | valid | 46784kb | alexk | 0.08 | 0:00.09 |
| regression/symmetry_aware_cav12threader/03_peterson/test | 0 | 0 | 2 | 0 | 0 | 0 | 139 | SUCCESSFUL | 6 | 0 | 0 | 0.003 | 0.078 | 0.008 | 0.001 | 0 | 0.000735 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/03_peterson/test.bin | Thu Dec 8 21:20:59 GMT 2011 | 0 | valid | 46480kb | alexk | 0.16 | 0:00.09 |
| regression/symmetry_aware_cav12threader/04_szymanski/test | 0 | 0 | 2 | 0 | 0 | 0 | 473 | SUCCESSFUL | 7 | 0 | 0 | 0.011 | 0.145 | 0.012 | 0.001 | 0 | 0.002975 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/04_szymanski/test.bin | Thu Dec 8 21:21:00 GMT 2011 | 0 | valid | 52064kb | alexk | 0.23 | 0:00.17 |
| regression/symmetry_aware_cav12threader/05_read_write_lock/test | 0 | 0 | 3 | 0 | 0 | 0 | 81 | SUCCESSFUL | 7 | 0 | 0 | 0.004 | 0.141 | 0.022 | 0.001 | 0 | 0.000564 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/05_read_write_lock/test.bin | Thu Dec 8 21:21:02 GMT 2011 | 0 | valid | 44448kb | alexk | 0.36 | 0:00.17 |
| regression/symmetry_aware_cav12threader/06_time_var_mutex/test | 0 | 0 | 2 | 0 | 0 | 0 | 76 | SUCCESSFUL | 7 | 0 | 0 | 0.005 | 0.113 | 0.007 | 0.001 | 0 | 0.000622 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/06_time_var_mutex/test.bin | Thu Dec 8 21:21:03 GMT 2011 | 0 | valid | 46368kb | alexk | 0.15 | 0:00.12 |
| regression/symmetry_aware_cav12threader/07_bakery.simple/test | 0 | 0 | 24 | 0 | 0 | 0 | 2796 | SUCCESSFUL | 24 | 0 | 0 | 0.074 | 3.245 | 2.544 | 0.015 | 0 | 0.030119 | 94 | 20 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/07_bakery.simple/test.bin | Thu Dec 8 21:21:04 GMT 2011 | 0 | valid | 54080kb | alexk | 8.53 | 0:05.90 |
| regression/symmetry_aware_cav12threader/08_bakery/test | 123755 | 0 | 23 | 7 | 0 | 4 | 2311 | SUCCESSFUL | 17 | 0 | 0 | 0.094 | 38.519 | 7.686 | 0.02 | 17.5014 | 0.02882 | 167 | 19 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/08_bakery/test.bin | Thu Dec 8 21:21:11 GMT 2011 | 0 | valid | 197904kb | alexk | 58.03 | 0:46.35 |
| regression/symmetry_aware_cav12threader/09_lamport/test | 0 | 0 | 5 | 0 | 0 | 0 | 1117 | SUCCESSFUL | 11 | 0 | 0 | 0.016 | 0.304 | 0.144 | 0 | 0 | 0.007787 | 3 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/09_lamport/test.bin | Thu Dec 8 21:21:58 GMT 2011 | 0 | valid | 51152kb | alexk | 0.60 | 0:00.47 |
| regression/symmetry_aware_cav12threader/10_qrcu_2proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11373 | SUCCESSFUL | 13 | 0 | 0 | 0.152 | 4.696 | 1.287 | 0.01 | 1.25522 | 0.07076 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/10_qrcu_2proc/test.bin | Thu Dec 8 21:22:00 GMT 2011 | 0 | valid | 169136kb | alexk | 8.68 | 0:06.16 |
| regression/symmetry_aware_cav12threader/11_qrcu_3proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11357 | SUCCESSFUL | 13 | 0 | 0 | 0.155 | 4.684 | 1.274 | 0.011 | 1.25361 | 0.070698 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/11_qrcu_3proc/test.bin | Thu Dec 8 21:22:07 GMT 2011 | 0 | valid | 169152kb | alexk | 8.61 | 0:06.14 |
| regression/symmetry_aware_cav12threader/12_qrcu_4proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11367 | SUCCESSFUL | 14 | 0 | 0 | 0.176 | 5.062 | 1.323 | 0.011 | 1.30039 | 0.070518 | 41 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/12_qrcu_4proc/test.bin | Thu Dec 8 21:22:14 GMT 2011 | 0 | valid | 169888kb | alexk | 9.46 | 0:06.59 |
| regression/symmetry_aware_cav12threader/13_lu-fig2.fixed/test | 0 | 0 | 3 | 0 | 0 | 0 | 38 | SUCCESSFUL | 5 | 0 | 0 | 0.005 | 0.107 | 0.01 | 0.002 | 0 | 0.000206 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/13_lu-fig2.fixed/test.bin | Thu Dec 8 21:22:22 GMT 2011 | 0 | valid | 46528kb | alexk | 0.21 | 0:00.12 |
| regression/symmetry_aware_cav12threader/14_seesaw/test | 0 | 0 | 4 | 6 | 0 | 0 | 44732 | SUCCESSFUL | 0 | 0 | 0 | 0.074 | 6.971 | 0.036 | 0 | 0 | 0.590631 | 2 | 2 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/14_seesaw/test.bin | Thu Dec 8 21:22:23 GMT 2011 | 0 | valid | 890992kb | alexk | 7.29 | 0:07.09 |
| regression/symmetry_aware_cav12threader/15_scull/test | 0 | 0 | 6 | 9 | 0 | 0 | 2311 | SUCCESSFUL | 5 | 0 | 0 | 0.114 | 0.756 | 0.494 | 0.009 | 0 | 0.018231 | 6 | 3 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/15_scull/test.bin | Thu Dec 8 21:22:31 GMT 2011 | 0 | valid | 74752kb | alexk | 1.77 | 0:01.40 |
| regression/symmetry_aware_threader_ready/01_inc/test | 98 | 0 | 7 | 2 | 0 | 2 | 451 | SUCCESSFUL | 5 | 0 | 0 | 0.028 | 0.34 | 0.775 | 0.004 | 0.007277 | 0.002889 | 12 | 4 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/01_inc/test.bin | Thu Dec 8 21:22:34 GMT 2011 | 0 | valid | 52272kb | alexk | 1.26 | 0:01.15 |
| regression/symmetry_aware_threader_ready/02_inc_cas/test | 322 | 0 | 7 | 4 | 0 | 2 | 254 | SUCCESSFUL | 0 | 0 | 0 | 0.013 | 0.358 | 0.412 | 0.003 | 0.062662 | 0.001741 | 21 | 4 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/02_inc_cas/test.bin | Thu Dec 8 21:22:36 GMT 2011 | 0 | valid | 69328kb | alexk | 0.88 | 0:00.79 |
| regression/symmetry_aware_threader_ready/03_incdec/test | 2301 | 0 | 16 | 4 | 0 | 3 | 3226 | SUCCESSFUL | 9 | 0 | 0 | 0.085 | 2.336 | 3.778 | 0.013 | 0.697289 | 0.02833 | 43 | 12 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/03_incdec/test.bin | Thu Dec 8 21:22:38 GMT 2011 | 0 | valid | 119616kb | alexk | 7.17 | 0:06.23 |
| regression/symmetry_aware_threader_ready/04_incdec_cas/test | 42458 | 0 | 24 | 8 | 0 | 4 | 11208 | SUCCESSFUL | 2 | 0 | 0 | 0.061 | 31.089 | 5.139 | 0.022 | 18.5363 | 0.071535 | 108 | 19 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/04_incdec_cas/test.bin | Thu Dec 8 21:22:45 GMT 2011 | 0 | valid | 1235536kb | alexk | 40.68 | 0:36.34 |
| regression/symmetry_aware_threader_ready/05_tas/test | 358 | 0 | 3 | 1 | 0 | 1 | 493 | SUCCESSFUL | 4 | 0 | 0 | 0.011 | 0.216 | 0.011 | 0.002 | 0.019284 | 0.003604 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/05_tas/test.bin | Thu Dec 8 21:23:22 GMT 2011 | 0 | valid | 65504kb | alexk | 0.31 | 0:00.24 |
| regression/symmetry_aware_threader_ready/06_ticket/test | 15605 | 0 | 9 | 2 | 0 | 5 | 9738 | SUCCESSFUL | 9 | 0 | 0 | 0.199 | 12.171 | 2.154 | 0.047 | 5.55223 | 0.074647 | 44 | 6 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/06_ticket/test.bin | Thu Dec 8 21:23:24 GMT 2011 | 0 | valid | 423824kb | alexk | 18.00 | 0:14.58 |
| regression/symmetry_aware_threader_ready/07_rand/test | 0 | 0 | 4 | 8 | 0 | 0 | 1363 | SUCCESSFUL | 3 | 0 | 0 | 0.083 | 0.217 | 0.975 | 0.006 | 0 | 0.009151 | 5 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/07_rand/test.bin | Thu Dec 8 21:23:39 GMT 2011 | 0 | valid | 79488kb | alexk | 1.30 | 0:01.29 |
| regression/symmetry_aware_threader_ready/08_rand_cas/test | 0 | ERROR | 0 | 0 | -6 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/08_rand_cas/test.bin | Thu Dec 8 21:23:42 GMT 2011 | 130 | valid | 5398112kb | alexk | 1844.30 | 30:00.06 | ||||||||||||||
| regression/symmetry_aware_threader_ready/09_fmaxsym/test | 283 | 0 | 3 | 6 | 0 | 7 | 2306 | SUCCESSFUL | 2 | 0 | 0 | 0.163 | 0.547 | 0.177 | 0.019 | 0.157177 | 0.018021 | 2 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/09_fmaxsym/test.bin | Thu Dec 8 21:53:43 GMT 2011 | 0 | valid | 104400kb | alexk | 1.04 | 0:00.91 |
| regression/symmetry_aware_threader_ready/10_fmaxsym_cas/test | 6118 | 0 | 13 | 2 | 0 | 4 | 7056 | SUCCESSFUL | 0 | 0 | 0 | 0.049 | 7.246 | 1.009 | 0.097 | 3.70893 | 0.059345 | 45 | 9 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/10_fmaxsym_cas/test.bin | Thu Dec 8 21:53:45 GMT 2011 | 0 | valid | 403728kb | alexk | 9.20 | 0:08.41 |
| regression/symmetry_aware_threader_ready/11_fmaxsymopt/test | 378 | 0 | 3 | 2 | 0 | 1 | 5065 | SUCCESSFUL | 2 | 0 | 0 | 0.045 | 0.45 | 0.194 | 0.02 | 0.022529 | 0.028641 | 2 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/11_fmaxsymopt/test.bin | Thu Dec 8 21:53:54 GMT 2011 | 0 | valid | 109728kb | alexk | 0.80 | 0:00.71 |
| regression/symmetry_aware_threader_ready/12_fmaxsymopt_cas/test | 9693 | 0 | 9 | 3 | 0 | 4 | 1904 | SUCCESSFUL | 0 | 0 | 0 | 0.048 | 12.731 | 1.193 | 0.07 | 9.91664 | 0.011387 | 37 | 5 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/12_fmaxsymopt_cas/test.bin | Thu Dec 8 21:53:56 GMT 2011 | 0 | valid | 315872kb | alexk | 14.76 | 0:14.05 |
| regression/symmetry_aware_threader_ready/13_stack/test | 0 | 0 | 5 | 6 | 0 | 0 | 125217 | SUCCESSFUL | 6 | 0 | 0 | 0.025 | 10.948 | 0.093 | 0.01 | 0 | 0.984845 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/13_stack/test.bin | Thu Dec 8 21:54:11 GMT 2011 | 0 | valid | 1689648kb | alexk | 11.23 | 0:11.08 |
| regression/symmetry_aware_threader_ready/14_stack_cas/test | 9077 | 0 | 7 | 6 | 0 | 1 | 105523 | SUCCESSFUL | 4 | 0 | 0 | 0.025 | 12.675 | 0.176 | 0.015 | 1.83356 | 0.807604 | 4 | 3 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/14_stack_cas/test.bin | Thu Dec 8 21:54:23 GMT 2011 | 0 | valid | 1665520kb | alexk | 13.06 | 0:12.90 |
| regression/symmetry_aware_threader_ready/15_unverif/test | 374 | 0 | 4 | 0 | 0 | 2 | 515 | SUCCESSFUL | 3 | 0 | 0 | 0.008 | 0.299 | 0.103 | 0.001 | 0.018358 | 0.003465 | 14 | 2 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 3 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/15_unverif/test.bin | Mon Dec 19 11:41:33 GMT 2011 | 0 | valid | 54768kb | alexk | 0.55 | 0:00.41 |