| * satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 version 3.0 results * Timeout: 1800s Memory limit: unlimitedkb Fri Jan 27 17:19:08 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 | 47 | SUCCESSFUL | 3 | 0 | 0 | 0.001 | 0.052 | 0.006 | 0 | 0 | 0.000385 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/01_spin2003/test.bin | Thu Dec 8 21:16:48 GMT 2011 | 0 | valid | 45968kb | alexk | 0.07 | 0:00.06 |
| regression/symmetry_aware_cav12threader/02_dekker/test | 0 | 0 | 2 | 0 | 0 | 0 | 133 | SUCCESSFUL | 5 | 0 | 0 | 0.005 | 0.06 | 0.008 | 0.001 | 0 | 0.000605 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/02_dekker/test.bin | Thu Dec 8 21:16:49 GMT 2011 | 0 | valid | 46592kb | alexk | 0.09 | 0:00.07 |
| regression/symmetry_aware_cav12threader/03_peterson/test | 0 | 0 | 2 | 0 | 0 | 0 | 75 | SUCCESSFUL | 6 | 0 | 0 | 0.004 | 0.066 | 0.008 | 0 | 0 | 0.0006 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/03_peterson/test.bin | Thu Dec 8 21:16:50 GMT 2011 | 0 | valid | 46480kb | alexk | 0.11 | 0:00.08 |
| regression/symmetry_aware_cav12threader/04_szymanski/test | 0 | 0 | 2 | 0 | 0 | 0 | 473 | SUCCESSFUL | 7 | 0 | 0 | 0.011 | 0.087 | 0.011 | 0.001 | 0 | 0.002649 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/04_szymanski/test.bin | Thu Dec 8 21:16:51 GMT 2011 | 0 | valid | 52048kb | alexk | 0.08 | 0:00.11 |
| regression/symmetry_aware_cav12threader/05_read_write_lock/test | 0 | 0 | 3 | 0 | 0 | 0 | 55 | SUCCESSFUL | 7 | 0 | 0 | 0.006 | 0.119 | 0.021 | 0 | 0 | 0.00039 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/05_read_write_lock/test.bin | Thu Dec 8 21:16:52 GMT 2011 | 0 | valid | 44464kb | alexk | 0.17 | 0:00.15 |
| regression/symmetry_aware_cav12threader/06_time_var_mutex/test | 0 | 0 | 2 | 0 | 0 | 0 | 138 | SUCCESSFUL | 7 | 0 | 0 | 0.005 | 0.072 | 0.007 | 0 | 0 | 0.00075 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/06_time_var_mutex/test.bin | Thu Dec 8 21:16:54 GMT 2011 | 0 | valid | 46352kb | alexk | 0.13 | 0:00.08 |
| regression/symmetry_aware_cav12threader/07_bakery.simple/test | 0 | 0 | 24 | 0 | 0 | 0 | 2796 | SUCCESSFUL | 24 | 0 | 0 | 0.076 | 3.144 | 2.533 | 0.014 | 0 | 0.030181 | 94 | 20 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/07_bakery.simple/test.bin | Thu Dec 8 21:16:55 GMT 2011 | 0 | valid | 54080kb | alexk | 8.33 | 0:05.78 |
| regression/symmetry_aware_cav12threader/08_bakery/test | 123755 | 0 | 23 | 7 | 0 | 4 | 2311 | SUCCESSFUL | 17 | 0 | 0 | 0.097 | 37.926 | 7.706 | 0.018 | 17.387 | 0.028971 | 167 | 19 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/08_bakery/test.bin | Thu Dec 8 21:17:02 GMT 2011 | 0 | valid | 197920kb | alexk | 56.76 | 0:45.77 |
| regression/symmetry_aware_cav12threader/09_lamport/test | 0 | 0 | 5 | 0 | 0 | 0 | 1117 | SUCCESSFUL | 11 | 0 | 0 | 0.015 | 0.278 | 0.145 | 0.002 | 0 | 0.007053 | 3 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/09_lamport/test.bin | Thu Dec 8 21:17:48 GMT 2011 | 0 | valid | 50960kb | alexk | 0.50 | 0:00.44 |
| regression/symmetry_aware_cav12threader/10_qrcu_2proc/test | 9102 | 0 | 11 | 10 | 0 | 2 | 11391 | SUCCESSFUL | 13 | 0 | 0 | 0.154 | 4.502 | 1.267 | 0.009 | 1.25392 | 0.070887 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/10_qrcu_2proc/test.bin | Thu Dec 8 21:17:50 GMT 2011 | 0 | valid | 169136kb | alexk | 8.27 | 0:05.95 |
| regression/symmetry_aware_cav12threader/11_qrcu_3proc/test | 9102 | 0 | 11 | 10 | 0 | 2 | 11391 | SUCCESSFUL | 13 | 0 | 0 | 0.157 | 4.496 | 1.306 | 0.01 | 1.25251 | 0.070996 | 40 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/11_qrcu_3proc/test.bin | Thu Dec 8 21:17:57 GMT 2011 | 0 | valid | 169136kb | alexk | 8.26 | 0:05.98 |
| regression/symmetry_aware_cav12threader/12_qrcu_4proc/test | 9101 | 0 | 11 | 10 | 0 | 2 | 11367 | SUCCESSFUL | 14 | 0 | 0 | 0.18 | 4.843 | 1.333 | 0.011 | 1.30459 | 0.070488 | 41 | 7 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/12_qrcu_4proc/test.bin | Thu Dec 8 21:18:04 GMT 2011 | 0 | valid | 169888kb | alexk | 8.90 | 0:06.39 |
| regression/symmetry_aware_cav12threader/13_lu-fig2.fixed/test | 0 | 0 | 3 | 0 | 0 | 0 | 62 | SUCCESSFUL | 5 | 0 | 0 | 0.004 | 0.082 | 0.011 | 0 | 0 | 0.000337 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/13_lu-fig2.fixed/test.bin | Thu Dec 8 21:18:11 GMT 2011 | 0 | valid | 46528kb | alexk | 0.15 | 0:00.10 |
| regression/symmetry_aware_cav12threader/14_seesaw/test | 0 | 0 | 4 | 6 | 0 | 0 | 1262 | SUCCESSFUL | 0 | 0 | 0 | 0.072 | 0.314 | 0.033 | 0.002 | 0 | 0.007878 | 2 | 2 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/14_seesaw/test.bin | Thu Dec 8 21:18:13 GMT 2011 | 0 | valid | 73424kb | alexk | 0.57 | 0:00.43 |
| regression/symmetry_aware_cav12threader/15_scull/test | 0 | 0 | 1 | 0 | 0 | 0 | 7 | SUCCESSFUL | 3 | 0 | 0 | 0.028 | 0.042 | 0 | 0 | 0 | 4.8e-05 | 0 | 0 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_cav12threader/15_scull/test.bin | Thu Dec 8 21:18:14 GMT 2011 | 0 | valid | 49040kb | alexk | 0.12 | 0:00.08 |
| regression/symmetry_aware_threader_ready/01_inc/test | 79 | 0 | 7 | 2 | 0 | 2 | 341 | SUCCESSFUL | 5 | 0 | 0 | 0.026 | 0.296 | 0.771 | 0.005 | 0.003463 | 0.001927 | 12 | 4 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/01_inc/test.bin | Thu Dec 8 21:18:15 GMT 2011 | 0 | valid | 47184kb | alexk | 1.17 | 0:01.10 |
| regression/symmetry_aware_threader_ready/02_inc_cas/test | 133 | 0 | 7 | 4 | 0 | 2 | 154 | SUCCESSFUL | 0 | 0 | 0 | 0.014 | 0.255 | 0.41 | 0.003 | 0.008985 | 0.000904 | 21 | 4 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/02_inc_cas/test.bin | Thu Dec 8 21:18:17 GMT 2011 | 0 | valid | 49344kb | alexk | 0.75 | 0:00.68 |
| regression/symmetry_aware_threader_ready/03_incdec/test | 1739 | 0 | 16 | 4 | 0 | 3 | 2396 | SUCCESSFUL | 9 | 0 | 0 | 0.084 | 1.523 | 3.785 | 0.016 | 0.125108 | 0.018762 | 43 | 12 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/03_incdec/test.bin | Thu Dec 8 21:18:19 GMT 2011 | 0 | valid | 61568kb | alexk | 6.18 | 0:05.43 |
| regression/symmetry_aware_threader_ready/04_incdec_cas/test | 18032 | 0 | 24 | 8 | 0 | 4 | 8381 | SUCCESSFUL | 2 | 0 | 0 | 0.062 | 8.472 | 4.88 | 0.024 | 3.84193 | 0.04982 | 108 | 19 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/04_incdec_cas/test.bin | Thu Dec 8 21:18:26 GMT 2011 | 0 | valid | 158320kb | alexk | 17.74 | 0:13.46 |
| regression/symmetry_aware_threader_ready/05_tas/test | 55 | 0 | 3 | 1 | 0 | 1 | 83 | SUCCESSFUL | 4 | 0 | 0 | 0.01 | 0.111 | 0.012 | 0 | 0.001659 | 0.000526 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/05_tas/test.bin | Thu Dec 8 21:18:40 GMT 2011 | 0 | valid | 47632kb | alexk | 0.17 | 0:00.13 |
| regression/symmetry_aware_threader_ready/06_ticket/test | 29 | 0 | 3 | 2 | 0 | 2 | 295 | SUCCESSFUL | 5 | 0 | 0 | 0.075 | 0.215 | 0.177 | 0.008 | 0.001354 | 0.00186 | 3 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/06_ticket/test.bin | Thu Dec 8 21:18:41 GMT 2011 | 0 | valid | 50256kb | alexk | 0.60 | 0:00.48 |
| regression/symmetry_aware_threader_ready/07_rand/test | 0 | 0 | 4 | 8 | 0 | 0 | 228 | SUCCESSFUL | 3 | 0 | 0 | 0.083 | 0.118 | 0.965 | 0.009 | 0 | 0.001448 | 5 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/07_rand/test.bin | Thu Dec 8 21:18:43 GMT 2011 | 0 | valid | 49936kb | alexk | 1.24 | 0:01.18 |
| regression/symmetry_aware_threader_ready/08_rand_cas/test | 96175 | 0 | 16 | 15 | 0 | 1 | 24530 | SUCCESSFUL | 2 | 0 | 0 | 0.254 | 93.005 | 23.889 | 0.027 | 36.3952 | 0.196893 | 68 | 10 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/08_rand_cas/test.bin | Thu Dec 8 21:18:45 GMT 2011 | 0 | valid | 775632kb | alexk | 140.64 | 1:57.19 |
| regression/symmetry_aware_threader_ready/09_fmaxsym/test | 64 | 0 | 3 | 6 | 0 | 7 | 257 | SUCCESSFUL | 2 | 0 | 0 | 0.163 | 0.215 | 0.177 | 0.019 | 0.00727 | 0.001804 | 2 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/09_fmaxsym/test.bin | Thu Dec 8 21:20:43 GMT 2011 | 0 | valid | 52192kb | alexk | 0.63 | 0:00.58 |
| regression/symmetry_aware_threader_ready/10_fmaxsym_cas/test | 1111 | 0 | 13 | 2 | 0 | 4 | 2968 | SUCCESSFUL | 0 | 0 | 0 | 0.047 | 1.353 | 1.014 | 0.098 | 0.081261 | 0.018188 | 45 | 9 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/10_fmaxsym_cas/test.bin | Thu Dec 8 21:20:45 GMT 2011 | 0 | valid | 89168kb | alexk | 3.08 | 0:02.52 |
| regression/symmetry_aware_threader_ready/11_fmaxsymopt/test | 77 | 0 | 3 | 2 | 0 | 1 | 589 | SUCCESSFUL | 2 | 0 | 0 | 0.045 | 0.169 | 0.192 | 0.02 | 0.002246 | 0.003019 | 2 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/11_fmaxsymopt/test.bin | Thu Dec 8 21:20:48 GMT 2011 | 0 | valid | 50288kb | alexk | 0.46 | 0:00.43 |
| regression/symmetry_aware_threader_ready/12_fmaxsymopt_cas/test | 1053 | 0 | 9 | 3 | 0 | 4 | 1805 | SUCCESSFUL | 0 | 0 | 0 | 0.047 | 0.877 | 1.189 | 0.068 | 0.115041 | 0.010632 | 37 | 5 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/12_fmaxsymopt_cas/test.bin | Thu Dec 8 21:20:50 GMT 2011 | 0 | valid | 70576kb | alexk | 2.65 | 0:02.19 |
| regression/symmetry_aware_threader_ready/13_stack/test | 0 | 0 | 5 | 6 | 0 | 0 | 4532 | SUCCESSFUL | 6 | 0 | 0 | 0.025 | 0.36 | 0.092 | 0.009 | 0 | 0.029173 | 1 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/13_stack/test.bin | Thu Dec 8 21:20:53 GMT 2011 | 0 | valid | 106592kb | alexk | 0.57 | 0:00.49 |
| regression/symmetry_aware_threader_ready/14_stack_cas/test | 440 | 0 | 7 | 6 | 0 | 1 | 4144 | SUCCESSFUL | 4 | 0 | 0 | 0.023 | 0.613 | 0.17 | 0.013 | 0.034125 | 0.0271 | 4 | 3 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/14_stack_cas/test.bin | Thu Dec 8 21:20:55 GMT 2011 | 0 | valid | 104672kb | alexk | 0.95 | 0:00.83 |
| regression/symmetry_aware_threader_ready/15_unverif/test | 58 | 0 | 3 | 0 | 0 | 2 | 147 | SUCCESSFUL | 3 | 0 | 0 | 0.007 | 0.133 | 0.045 | 0.001 | 0.00153 | 0.000793 | 7 | 1 | satabs -DSATABS --full-inlining --concurrency --iterations 1000 --csv-stats --save-bps --32 --max-threads 2 /home/alexk/sapa_toolpaper/build/regression/symmetry_aware_threader_ready/15_unverif/test.bin | Mon Dec 19 11:41:32 GMT 2011 | 0 | valid | 46640kb | alexk | 0.31 | 0:00.19 |